(declare-fun tval () (_ FloatingPoint 8 24))
(assert (fp.eq tval ((_ to_fp 8 24) roundNearestTiesToEven (/ 4067395 16777216))))
(declare-fun one () (_ FloatingPoint 8 24))
(assert (fp.eq one ((_ to_fp 8 24) roundNearestTiesToEven (/ 1 1))))
(declare-fun xval () (_ FloatingPoint 8 24))
(assert (fp.eq xval ((_ to_fp 8 24) roundNearestTiesToEven (/ 12113169 8388608))))
(declare-fun yval () (_ FloatingPoint 8 24))
(assert (fp.eq yval ((_ to_fp 8 24) roundNearestTiesToEven (/ 8109701 2097152))))
(declare-fun badzval () (_ FloatingPoint 8 24))
(assert (fp.eq badzval ((_ to_fp 8 24) roundNearestTiesToEven (/ 4217779 134217728))))
(declare-fun z () (_ FloatingPoint 8 24))
(declare-fun t () (_ FloatingPoint 8 24))
(declare-fun rhs () (_ FloatingPoint 8 24))
(assert (fp.eq rhs (fp.fma roundNearestTiesToEven xval (fp.sub roundNearestTiesToEven one t) (fp.mul roundNearestTiesToEven yval t))))
(assert (and (fp.eq t tval) (fp.eq z rhs) (fp.lt z xval)))
(check-sat)
